\begin{tabbing}
@$i$ only $L$ affect $x$:$T$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}dtype(${\it es}$; $i$; $x$; $T$)\+
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(($\neg$(es{-}kind(${\it es}$; $e$) $\in$ $L$)) $\Rightarrow$ (es{-}after(${\it es}$; $x$; $e$) = es{-}when(${\it es}$; $x$; $e$))))
\-\-
\end{tabbing}